
\documentclass[runningheads]{llncs}
\usepackage{stmaryrd}
\usepackage{amsfonts}

\usepackage{amssymb}
\setcounter{tocdepth}{3}
\usepackage{graphicx}
\usepackage{algorithmic, algorithm}

\usepackage{url}
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}

\begin{document}

\mainmatter  % start of an individual contribution

% first the title is needed
\title{Using Existing Characteristics of Domain-Specific Language to Verify Properties}

% a short form should be given in case it is too long for the running head
\titlerunning{Using Existing Characteristics of DSL to Verify Properties}

% the name(s) of the author(s) follow(s) next
%
% NB: Chinese authors should write their first names(s) in front of
% their surnames. This ensures that the names appear correctly in
% the running heads and the author index.
%
\author{}
%
\authorrunning{}
% (feature abused for this document to repeat the title also on left hand pages)

% the affiliations are given next; don't give your e-mail address
% unless you accept that it will be published
\institute{}

\toctitle{} \tocauthor{} \maketitle


\begin{abstract}

This paper presents a domain-specific language Pantagruel -- an
visual program language for pervasive computing environment -- and
its associated verification methods. Some characteristics and four
main static properties (conflict free, termination, dead code and
dead-lock) of Pantagruel are introduced. The verification methods
are so designed that they use the characteristics of Pantagruel
which makes the verification process much easier than that of an
general purpose language.

\keywords{Domain-Specific Language, Verification, Model Checking}
\end{abstract}

\section{Introduction}

\subsection{Domain-Specific Languages}

The DSL approach has long been used with great success in many
domains, from the telephony to web application development. Unlike
general-purpose programming languages, their goal is to provide a
restricted vocabulary that is adapted to the domain for which they
are dedicated, and thus target experts in that domain. Required
programming expertise vary according either to either the domain of
DSL, its vocabulary or its syntax. Popular DSLs are SQL (Structured
Query Language), specific to the manipulation of relational
databases, or GraphViz, a language to write graphs.

Advantages of DSL include the following:

\begin{itemize}
\item Language vocabulary is close to the domain expert vocabulary, therefore
more concise than general-purpose languages.
\item Verification is easier, and properties like Termination can become
decidable.
\end{itemize}

Other advantages can be found on the literature but these two are
the advantages that we are interested in.

\subsection{Pantagruel: a visual DSL for prototyping ubiquitous applications}

Ubiquitous computing is a domain that has become popular for recent
years, with the proliferation of remotely accessible, networked
devices that become programmable and interoperable. Networks of such
devices are deployed in various areas that we call ubiquitous
environments (or smart spaces). These environments aim at providing
various services to people living in there. A classic example is
home assistance e.g managing lights, heat, or helping residents in
their everyday-life activities by e.g. automating some of their
usual tasks.

Ubiquitous computing concerns different kinds of people, from
distributed computing experts to the end-users, i.e people living in
an ubiquitous environment. Therefore integrating DSL into this area
sounds accurate, in particular regarding end-users, since they can
now become programmers of their environment.

This motivated us to propose Pantagruel, a domain specific language
for prototyping ubiquitous application at an early stage of design.
Actually we do not directly target end-users, but designers whose
work is close to end-users and directly related to their
requirements. We place our language on early design stage where
end-user holds an important place. Therefore we introduced in our
language very high-level concepts that abstract over heterogeneity
of entities and intricacies of distributed computing.

There exists two forms of implementation of a DSL, that are either
embedding a DSL into an existing language or designing a standalone
DSL [TODO Zoe]. Embedded DSLs leverage the existing concepts of
general-purpose language and the various tools that are developed
for them. They are particularly suited to design DSLs whose target
is programmers that are already familiar to paradigms of the
embedding language. We adopted the embedding approach in Pantagruel.

\subsection{Verification}

Why we need verification.

Static and dynamic properties of DSL. [TODO Hai]

Recall the design philosophy of Pantagruel that Pantagruel is a
visual DSL for prototyping ubiquitous applications. By prototyping,
we mean we want the system as soon as possible. As a counterpart of
design, verification also needs to be done as soon as possible.

\section{Pantagruel in General}
\label{pan_in_general}

[TODO Zoe, in this section, I think you should say something about
the \emph{completed framework} which is archived by filling the
holes of the \emph{empty framework} generated by Pantagruel.]

Pantagruel is a rule-based language for prototyping ubiquitous
applications in two steps: first, the programmer defines an
environment as a collection of entity classes and their instances,
provided with their characteristics and functionalities. Second, the
programmer defines an orchestration logic on the instances. We won't
get deep in the details of this process. We will focus on this paper
on Pantagruel semantics, that specifies the execution process of the
orchestration logic. Before that, we rapidly introduce the concepts
of our language:

\paragraph{Entity classes.} Entity classes are abstractions of entities
that are contained in a pervasive environment. An entity class
consists of attributes defining a state and method interfacess to
invoke external operations. Attributes and methods are attached
annotations declaring information on their behavior. These classes
represent the building blocks required to define a coordination
scenario. An instance of an entity class is an entity for which
constant attributes are initialized.

\paragraph{Orchestration logic.} An orchestration logic or scenario consists of
a set of rules. Each rule has three parts: (1) a sensor, defining a
condition to trigger the rule, (2) a controller, combining sensors,
and (3) an actuator, performing some actions. In the following
section, we describe more precisely entity classes and the
orchestration logic.

\subsubsection{Definition of entity classes}

In this step, we build the taxonomy of entities that we want to
orchestrate. The taxonomy consists of a set of entity classes that
are hierarchically related to each other. Each class consists of
attributes and methods. There is a root class called \emph{Entity}
of which all entities inherit directly or indirectly. This hierarchy
allow reuse of attributes and methods

\paragraph{Attributes}

A class can have three kinds of attributes.  We refer to these kinds
with \emph{constant}, \emph{volatile}, and \emph{write} attributes.
Attributes are typed with primitive types (Integer, String, Boolean)
or user-defined enumerations.

\begin{itemize}
\item\emph{Constant attributes} are the variation points
between the instances of a given class. They represent fixed
characteristics that do not evolve across time.

\item\emph{Volatile attributes} abstract changes
of an entity characteristics whose origin comes from outside the
program. They represent data resulting from a reaction to external
stimuli.

\item\emph{Write attributes} represent the result of internal reactions (i.e.
internal occurring events) of the system described by Pantagruel
scenarios. These variables are modified by methods that declare them
as \emph{effects}, as mentioned in next paragraph.
\end{itemize}


\paragraph{Methods}
[TODO Zoe: list the types of specifications of methods:
1)modifies a set of write attributes; 2) modifies a write attribute
to a specific value]
Methods refer to external functions defined in external libraries of
Pantagruel runtime layer. It is not the role of Pantagruel to define
the behavior of these methods, but only to provide their
side-effects so that the designer of the orchestration logic is
aware of the effects a method can have on a Pantagruel program's
behavior. Methods can only modify \emph{write} attributes.
Therefore, the side-effects of a method are a set of write
attributes that belong to the method's class. A method can have
parameters.

\subsubsection{Defining an orchestration logic}

Once a set of entity classes are defined as well as a collection of
instances, we can define the orchestration logic (= scenario). The
scenario describes the behavior of instances according to some
conditions in the form of rules. This part of Pantagruel borrows
heavily from Blender Game Engine\footnote{http://www.blender.org}, a
software for designing games and dedicated to novice- either
non-programmers.

A pantagruel scenario consists of defining a set of rules following
a paradigm called sensor-controller-actuator. A rule is a collection
of sensors that are combined with a controller. These sensors are
also connected to a set of actuators using this controller. Each
sensor is a condition on the attribute of an entity (or entity
class), and each actuator is a method invocation, and a controller
is a OR or AND logic operator: conditions in a rule can be pure
conjunctions or pure disjunctions, i.e they respectively all must be
satisfied, or only one of them, to trigger the actions execution. In
summary, all the methods used in a rule are executed when one or all
(depending on the controller) of the conditions of this rule are
satisfied (we give details of the rule execution process in Section
\ref{characteristics}).

\subsubsection{Informal Dynamic Semantics of Pantagruel}

Give an informal dynamic semantics of Pangruel here. [TODO Zoe]

\section{Characteristics of Pantagruel}

Give some descriptions of the following characteristics of
Pantagruel and also give some convincing reasons that why Pantagruel
should have such characteristics. [TODO Zoe]

\subsection{Initialization of write attributes}

Why do not we have a fix initialization of all write attributes and
volatile attributes to $\bot$?

\subsection{Pure Conjunctions and Disjunctions}

Why do we have pure conjunction and disjunction.

\subsection{Rule Trigger Condition}

Why we design the trigger semantics like this (a rule is triggered
iff it current precondition is true and its previous precondition is
false)?

\section{Static Properties of Pantagruel}

In this section, we informally introduce four main static properties
of Pantagruel, say, termination, dead rule and dead-lock. We will
give a formal definition of these properties in next section.

\paragraph{Conflict free} In Pantagruel, we can mark some rules as
conflict set, which means two or more rules in that set cannot be
triggered at the same cycle. For example, there two rules that one
is used to turn on the light and the other is used to turn off the
light. These two rules cannot be triggered at the same cycle. In
Pantagruel, we can mark a set of conflict sets.

\paragraph{Termination} Termination means that the system won't loop
for ever. This informal description is proper for non-interactive
systems but not proper for interactive systems, such as Pantagruel.
In Pantagruel, termination is defined as: if the environment doesn't
change the volatile attributes after some time, then the system will
eventually stops, i.e. no rule can be triggered at all. The
motivation of this definition is demonstrated in
Fig.~\ref{fig:termination}. The changes of volatile attributes is
the reason why the system starts to trigger rules. The effects of
the triggered rule may modify some write attributes, which in turn
may lead to trigger of rules in the next cycle. If the environment
doesn't change volatile attributes after some time, which can be
denoted by removing the ``environment'' part in
Fig.~\ref{fig:termination}. If the system doesn't stop afterwards,
which means the system will always invoke some methods afterwards,
it is not a well-defined system behavior. For example, this may lead
to an infinite alternate on/off operations of light. The system
should have termination property.

\begin{figure}
\centering
\includegraphics[scale=0.8]{figtermination}
\caption{Description of termination}
\label{fig:termination}
\end{figure}

\paragraph{Dead rule} Dead rule is a rule that cannot be triggered
at all. Dead rules are not allowed in Pantagruel, since every rule
should represent some intended behaviors of the system.

\paragraph{Dead-lock} Dead-lock means the system can reach a
``pure'' stable state such that no matter how the environment
changes the volatile attributes there is no rule can be triggered.
Dead-lock makes the system not to respond any input of the
environment. Dead-lock is not allowed in the system.

\section{Formal Representation of Pantagruel}
\label{foraml_Pan}

In order to reason Pantagruel formally, we propose here a formal
representation of the conceptions introduced in the previous
sections. In particular, we do not take into account the notions of
entity classes and entities. Instead, we will reason on the
attributes as simple variables of the three mentioned kinds: write,
volatile, and constant. We consider constant attributes as constants
values, since after initialization constant attributes are replaced
by constants values. We first give the formal syntax, then give the
formal semantics. Finally, we give the formal definitions of the
four static properties we concern.

\subsection{Syntax}

\begin{definition}[Variable, constant and domain]
\label{d_1_variables} Variables are the attributes that Pantagruel
manipulates. The set of all variables and constants are denoted by
$V$ and $C$ respectively. Each variable $v$ in $V$ (constant $c$ in
$C$) has its own domain, which is denoted by $D_v$ ($D_c$). A
undefined value $\bot$ is added to every domain. A domain $D$ with
$\bot$ is denoted by $D_{\bot}$. There are 3 predefined domains:
$Int_{\bot}$ for integers, $Str_{\bot}$ for strings and $Bool_{\bot}
= \{true, false, \bot\}$ for Boolean.
\end{definition}

\begin{definition}[Operators]
\label{Ops}
There are 6 operators in Pantagruel: $<$, $>$, $=$,
$\neq$, $in$, $changed$. The set of operators is denoted by $O$.
\end{definition}

Given two sets $V$ and $C$, we can build terms and preconditions on
them.
\begin{definition}[Term]
\label{term_def} A term is of one of the following forms:
\begin{itemize}
\item ($x_1~op~x_2$), where $op \in \{<, >, =, \neq\} \wedge
x_1 \in V\cup C \wedge x_2 \in V\cup C \wedge op \in O \wedge
D_{x_1} = D_{x_2}$;
\item ($x~changed$), where $x \in V\cup C$;
\item ($x~ in ~S$), where $x \in V\cup C \wedge S \subseteq D_x$.
\end{itemize}

Given a term $t$, we use $V_t$ to represent the variables used in
$t$.

\end{definition}

\begin{definition}[Scenario] A scenario is a tuple $\Psi = (V, C, V_w, O, T, R, X)$. $V$ is a set of
variables which are used to represent the attributes used in a
scenario. $C$ is a set of constants. $V_w \subseteq V$ is used to
represent the write attributes. We introduce $V_v = V - V_w$ to
denote the write attributes. $O$ is defined in definition \ref{Ops}.
$T$ is a set of terms built on $V$ and $C$. $R$ is a set of rules.
$X \subseteq 2^R$ represent the set of conflict sets.

A rule is of one of the following forms, where $P \subseteq T$ and
$E \subseteq V_w$:

\begin{itemize}
\item $(\bigwedge_{t \in P} t) \rightarrow E$
\item $(\bigvee_{t \in P} t) \rightarrow E$

\end{itemize}

Given a rule r, the part before the arrow is called the precondition
of r, and the part after the arrow is called the effected set of r.
We use $P_r$, $E_r$ and $T_r$ to denote the precondition of r, the
effected set of r, and the set of terms used in r respectively.

Let $T^{wc} = \{t|t\in T \wedge \exists v\in V_w: t = v~ changed\}$
, $T^{vc} = \{v ~changed | v \in V_v\}$ and $T^n = T - T^{wc} -
T^{vc}$.


\end{definition}

Given a scenario $\Psi$, $V_\Psi$ is used to denote the element $V$
in $\Psi$. The same idea is used for the rest elements in $\Psi$.
From now no, we will reason on a fixed scenario $\Psi$. Hence, the
subscript $\Psi$ will be omitted if there is no ambiguity.


\begin{definition}[Empty-framework and completed-framework]
The empty-framework is the program written in the host language
generated by the scenario $\Psi$, which is denoted by $ef$. A
completed-framework of $s$ is the program with all empty methods in
$ef$ filled. The set of all completed-frameworks of $\Psi$ is
presented by $CF$.

\end{definition}

\subsection{Semantics}
In this section, we give the formal semantics of Pantagruel based on
the trace semantics. First we give the definition of system states.

\begin{definition}[States]
A state is a 2-tuple $(w, v)$. $w$ is a $|V_w|$-tuple which is a
valuation of all the write variables, where $|\bullet |$ is the
cardinality of set $\bullet $. $v$ is a $|V_v|$-tuple which is a
valuation of all the volatile variables. $S$ is used to denote the
set of all the states. A state $s$ can be represented as $\ll
w_1,w_2,...,w_{|V_w|}>,<v_1,v_2,...,v_{|V_v|}\gg$. We use $s(v)$ to
denote the value of variable $v$ at state $s$.

\end{definition}

In order to define the next state function and runs of the system,
we need the following auxiliary definitions based on the execution
model of Pantagruel.

\begin{definition}[Valuation of terms and preconditions]
The fact that the valuation of a term $t\in T$ is $true$ at two
states $s_1$ and $s_2$ is denoted by:

\begin{itemize}
\item $(s_1,s_2)\models t$, where $t$ is of form ``x changed'';
\item $s_2 \models t$, otherwise.
\end{itemize}

The interpretation of terms is defined as following (note that, if
$x$ is a constant and $s$ is a state, in order to save space we use
$s(x)$ to represent the constant.):

\begin{itemize}

\item $s_2\models (x_1 < x_2)$ iff $s_2(x_1) < s_2(x_2) \wedge s_2(x_1)\neq\bot\wedge s_2(x_2)\neq\bot$;
\item $s_2\models (x_1 > x_2)$ iff $s_2(x_1) > s_2(x_2) \wedge s_2(x_1)\neq\bot\wedge s_2(x_2)\neq\bot$;
\item $s_2\models (x_1 = x_2)$ iff $s_2(x_1) = s_2(x_2) \wedge s_2(x_1)\neq\bot\wedge s_2(x_2)\neq\bot$;
\item $s_2\models (x_1 \neq x_2)$ iff $s_2(x_1) \neq s_2(x_2) \wedge s_2(x_1)\neq\bot\wedge s_2(x_2)\neq\bot$;
\item $s_2\models (x ~in ~D)$ iff $s_2(x) \in D \wedge s_2(x)\neq\bot$;
\item $(s_1,s_2)\models (changed ~x)$ iff $s_1(x) \neq s_2(x)\wedge s_2(x)\neq\bot$.

\end{itemize}

If a term $t$ is not of the form ``x changed'', then
$(s_1,s_2)\models t \triangleq s_2\models t$.

A term $t$ is said disabled at a state s if $\exists v\in V_t, s(v)
= \bot$. It is obvious that $\forall t~ s_1~ s_2, t ~is~ disabled~
at~ s_2 \rightarrow (s_1,s_2)\not\models t$.

Given two states $s_1$ and $s_2$ and a rule $r$, the fact that the
valuation of the precondition $P_r$ of $r$ at $(s_1,s_2)$ is true is
denoted by $(s_1,s_2)\models P_r$. The interpretation of
preconditions is defined as following:

\begin{itemize}

\item $(s_1, s_2)\models \bigwedge_{t\in T_r} t$ iff $\forall t \in T_r: (s_1,
s_2)\models t$;
\item $(s_1, s_2)\models \bigvee_{t\in T_r} t$ iff $\exists  t \in T_r: (s_1,
s_2)\models t$.
\end{itemize}


\end{definition}

\begin{definition}[Active term]
Given two states $s_1$ and $s_2$, a term $t\in T_s$ is active at
$(s_1,s_2)$ iff one of the following condition holds:

\begin{itemize}

\item $(s_1, s_2)\models t$, where $t$ is of form ``$x~ changed$'';
\item $s_1 \not\models t \wedge s_2 \models t$, otherwise.

\end{itemize}
\end{definition}

\begin{definition}[Enabled rule]
Given 2 states $s_1$ and $s_2$, a rule r is enabled at states $(s_1,
s_2)$ iff $(s_1, s_2)\models P_r \wedge \exists t\in T_r: t ~is~
active$ at $(s_1,s_2)$.

\end{definition}

The pseudocode of the execution algorithm of Pantagruel is shown in
Algorithm \ref{algorithm}. Note that we only can execute the
completed-framework, since it is in a completed-framework that we
can know the next state of the current state explicitly. In the
empty-framework what we know of the methods is that they may modify
some write variables. In other words, we don't know which values the
write variables are set to after the execution of a method.

\begin{algorithm}
\caption{The execution algorithm of Pantagruel}
\label{algorithm}
\begin{algorithmic}[1]

\STATE Let $s$, $s_1$ and $s_2$ be 3 states. Initially, $s = s_1 =
s_2$ and $\forall v \in V: s(v)=\bot$.

\WHILE{true}

\FORALL{$r \in R$}

\IF{$r$ is enable at $(s_1, s_2)$}

\STATE $s \leftarrow eval\_rule(r, s)$

\ENDIF

\ENDFOR

\STATE $s \leftarrow update\_volatile(V_v, s)$

\STATE $s_1 \leftarrow copy(s_2)$

\STATE $s_2 \leftarrow copy(s)$

\ENDWHILE
\end{algorithmic}\end{algorithm}

With algorithm \ref{algorithm}, we can have the following notions.

\begin{definition}[Next state function, trace and run]
\label{Next_state_function_trace_run_def} Given a
completed-framework ~$cf \in CF$, a function $f_{cf}:S \rightarrow
S$ is used to represent the computation of calculating the next
state based on the current state. Note that $f_{cf}$ simulates both
the effects of the environment on volatile variables and the effects
of rules that are triggered on the write variables.

A trace is an infinite sequence of states: $s_0 \rightarrow s_1
\rightarrow \cdots $. $s[i]$, $s[\cdots i]$ and $s[i\cdots]$ are
used to denote the $i\emph{th}$ state, the prefix $s_0 \rightarrow
s_1 \rightarrow \cdots \rightarrow s_i$ and the suffix $s_i
\rightarrow s_{i+1} \rightarrow \cdots $ of a trace respectively.
Two traces $\tau_1$ and $\tau_2$ are equal iff $\forall i\in
\mathbb{N}: \tau_1[i]=\tau_2[i]$. Two prefixes $\tau_1[\cdots i_1]$
and $\tau_2[\cdots i_2]$ are equal iff $\exists k \in \mathbb{N}:
i_1 = k \wedge i_2 = k \wedge \forall i\in [0,\cdots, k]:
\tau_1[i]=\tau_2[i]$.

A run $\sigma$ is a trace such that $\forall v\in V: \sigma[0](v) =
\bot \wedge \forall i \in \mathbb{N}:
\sigma[i+1]=f_{cf}(\sigma[i])$. The set of all runs is denoted by
$\Delta_{cf}$.

Given a run $\sigma$, we represent the behavior of the environment
and the Pantagruel system by function $E_{\sigma} : \mathbb{N}
\rightarrow Bool$ and function $RT_{\sigma} : \mathbb{N} \rightarrow
R$ such that $E_{\sigma}(i) = true~$iff~$\exists v\in V_v:
\sigma[i](v) \neq \sigma[i+1](v)$ and $RT(i)$ is the rules that
triggered at cycle $i$.

\end{definition}

The semantics of a completed-framework $cf$ is described by its
runs: $\Delta_{cf}$.

\subsection{Formal Definitions of Static Properties}
\label{formal_def_properties}

In this section, we give the formal definitions of the four static
properties based on the definitions given in previous sections.

\begin{definition}[Conflict free]
A completed-framework $cf$ is conflict free iff $\forall C \in X,
r_1\in C, r_2 \in C, \sigma \in \Delta_{cf},i\in \mathbb{N}: r_1
\neq r_2 \rightarrow \neg (r_1 \in RT_\sigma(i) \wedge  r_2 \in
RT_\sigma(i))$.

A scenario $s$ is conflict free iff $\forall cf \in CF_s: cf ~is~
conflict ~free$.

\end{definition}

\begin{definition}[Dead rule]
A rule $r$ is a dead rule of a completed-framework $cf$ iff $\forall
\sigma \in \Delta_{cf},i\in \mathbb{N}: r \not\in RT_\sigma(i)$.

A rule $r$ is a dead rule of a scenario $s$ iff $\forall cf \in
CF_s: r ~is~ a ~dead ~rule ~of~ cf$.

\end{definition}

\begin{definition}[Termination]
A completed-framework $cf$ terminates iff $\forall \sigma \in
\Delta_{cf},i\in \mathbb{N}: (\forall j\in \mathbb{N}: i \le j
\rightarrow E_\sigma(j) = false) \rightarrow (\exists k\in
\mathbb{N}: i \le k \wedge RT_\sigma(k) = \emptyset )$.

A scenario $s$ terminates iff $\forall cf \in CF_s: cf~terminates$.

\end{definition}

\begin{definition}[Dead lock]
A completed-framework $cf$ has dead lock iff ~$\exists \sigma \in
\Delta_{cf}, i \in \mathbb{N}: (\forall \sigma' \in
\Delta_{cf}:\sigma[\cdots i] = \sigma'[\cdots i] \rightarrow \forall
j\in \mathbb{N}:i \le j \rightarrow RT_{\sigma'}(j)=\emptyset )$.

A scenario $s$ has a dead lock iff $\exists cf \in CF_s: cf~has~dead
lock.$

\end{definition}

\section{Verification of Properties}

From the property definitions in section \ref{formal_def_properties}
we can know that there is a link between the scenario and the
completed-frameworks. There is a universal quantifier ($\forall cf
\in CF_s$) in all definitions. Hence, a property of the
empty-framework is the property of all the completed-framework. For
instance, if we can verify that a scenario $s$ is dead lock free,
then we can say every completed-frameworks $CF_s$ is also dead lock
free. Since the set of completed-framework is infinite, it is
impossible to verify the properties of a scenario by checking all
its completed-frameworks. Hence, abstract model is needed to do
verification.

\subsection{Abstract Model of Scenario}

Let $\mathbb{T}$ be a set of terms. Variables in $V_\mathbb{T}$ form
a $|V_\mathbb{T}|$-dimension space and terms in $\mathbb{T}$ divide
the space into at most $2^{|\mathbb{T}|}$ disjoint regions each of
which can be identified by a unique function $r:
\mathbb{T}\rightarrow Bool$. A region consists of a set of states of
the space. It is clear that a state $s$ belongs to a region $r$ iff
$\forall t\in \mathbb{T}: r(t) = true\Leftrightarrow s \models t$.
Recall the definitions of $V, V_w$ and $V_v$ in previous sections,
we have the following auxiliary definitions.

\begin{definition}[Region and write/volatile-variables-changed status]
Given a set $\mathbb{T}$ of terms built on $V$ and a set $V_i$ of
initialized variables, a region which is represented by a function
$r$ of type ($\mathbb{T}\rightarrow Bool$) is a set of states of the
$|V|$-dimension space: $\{s|\forall t\in \mathbb{T}: V_t \subseteq
V_i \rightarrow (r(t)=true \leftrightarrow s \models t)\}$. The set
of all regions of $\mathbb{T}$ is denoted by $R^{V_i}_{\mathbb{T}}$.
It is clear that the cardinality of $R^{V_i}_{\mathbb{T}}$ is
finite. Each $r\in R^{V_i}_{\mathbb{T}}$ is called a region of
$\mathbb{T}$ and $V_i$.

Given a variable $v\in V$, the $v$-range of a region $r$ is of one
of the following forms:

\begin{itemize}
\item $[-\infty,+\infty]$, if $\forall c \in D_v: \exists s \in r:
s(v) < c \wedge \forall c \in D_v: \exists s \in r: s(v)
> c$
\item $[-\infty,c_r]$, if $\forall c \in D_v: \exists s \in r:
s(v) < c \wedge \forall s \in r: s(v) \le c_r \wedge \forall c \in
D_v: \forall s \in r: s(v) \le c \rightarrow c_r \le c$
\item $[c_l,+\infty]$, if $\forall c \in D_v: \exists s \in r:
s(v) > c \wedge \forall s \in r: s(v) \ge c_l \wedge \forall c \in
D_v: \forall s \in r: s(v) \ge c \rightarrow c_l \ge c$

\item $[c_l,c_r]$, if $
\forall s \in r: s(v) \ge c_l \wedge \forall c \in D_v: \forall s
\in r: s(v) \ge c \rightarrow c_l \ge c \wedge \forall s \in r: s(v)
\le c_r \wedge \forall c \in D_v: \forall s \in r: s(v) \le c
\rightarrow c_r \le c$
\end{itemize}

$v$-range is called right-bounded if it's of one of the forms
``$[-\infty,c_r]$'' and ``$[c_l,c_r]$''.

$v$-range is called right-unbounded if it's of one of the forms
``$[c_l, +\infty]$'' and ``$[-\infty,+\infty]$''.

$v$-range is called left-bounded if it's of one of the forms
``$[c_l,c_r]$'' and ``$[c_l,+\infty]$''.

$v$-range is called left-unbounded if it's of one of the forms
``$[-\infty, c_r]$'' and ``$[-\infty,+\infty]$''.


A write-variables-changed status is a function of type $(V_w
\rightarrow Bool)$. A volatile-variables-changed status is function
of type $(V_v \rightarrow Bool)$.

\end{definition}

Before introducing the abstract states, we need add some auxiliary
terms to $T^n$ to build a boundary of the finite regions:

\begin{itemize}

\item If there exists some constant used in $T^n$, then let $c_{max}$ and $c_{min}$ be the maximum and minimal
constants used in $T^n$.

\item For every variable $v\in V$, add two terms ``$v > c_{max}$'' and ``$v < c_{min}$'' to
$T^n$.

\item The new set of terms is denoted by $T^b$.

\end{itemize}

Then we have the following theorem:

\begin{theorem}

Given two regions $r_1, r_2 \in R^{V_i}_{\mathbb{T}}$ and any
variable $v \in V$, if $r_1$'s $v$-range is
left-bounded(right-bounded) and $r_2$'s $v$-range is
left-unbounded(right-unbounded), then $r_1$ and $r_2$'s $v$-ranges
are disjoint.

\end{theorem}

\begin{proof}
Omitted for now.[TODO Hai]
\end{proof}

\begin{definition}[Abstract states]
\label{def_ab_states} An abstract state is of the form $(V_i, r,
r',c_w,c_v,r_r)$, where $r$ and $r'$ are regions of $T^b$ and $V_i$,
$c_w$ is a write-variables-changed status, $c_v$ is a
volatile-variables-changed status and $r_r$ is an element of the set
$R_r$ which is built following the steps:

\begin{enumerate}
\item $\mathbb{T} = T^b$;
\item for each $v\in V$, if $r'$'s $v$-range is $[c_l,c_r]$,
then for each $c \in [c_l,c_r]$, add the term ``$v > c$'' to
$\mathbb{T}$;
\item $R_r = \{g:\mathbb{T} \rightarrow Bool~|~\forall t \in \mathbb{T}: t \in T^b
\rightarrow g(t) = r'(t)\}$.
\end{enumerate}
The set of all abstract states is denoted by $\mathcal{A}$.

\end{definition}

Intuitively, if the system is at cycle $i$ and its abstract state is
$(V_i,r,r',c_w,c_v,r_r)$, $V_i$ is the set of variables that have
been initialized, $r$ represents the previous region at cycle
$(i-1)$, $r'$ represents the current region and $r_r$ represents the
reachable region at cycle $i$. The idea of the reachable region is
that we use it to keep trace of the set of reachable concrete states
at cycle $i$. In other words, for each concrete state in the
reachable region we can find a concrete trace leading to it, which
makes our abstract model complete.

\begin{theorem}
The cardinality of $\mathcal {A}$ is finite.
\end{theorem}
\begin{proof}
Omitted for now.[TODO Hai]
\end{proof}

\begin{definition}[Abstract next state function]
$f^{\alpha}:\mathcal {A}\rightarrow 2^{\mathcal {A}}$ is the
abstract next state function.

Given an abstract state $\alpha \in \mathcal{A}$, its set of next
states is computed by the following steps:

\begin{enumerate}
\item Calculate the set $Rl$ of rules that can be triggered at
$\alpha$.

\item $V_{mod} = \bigcup_{r \in Rl} E_r$.

\item $V_{mod} = V_{mod} + V_v$.

\item $V^{new}_i = V_{mod} - \alpha.V_i$.

\item $V_i = {\alpha}.{V_i} + V_{mod}$.

\item $CW = \{s:V_w \rightarrow Bool~|~\forall v\in V^{new}_i \rightarrow
s(v)=true\}$.

\item $CV = \{s:V_v \rightarrow Bool~|~\forall v\in V^{new}_i \rightarrow
s(v)=true\}$.

\item for each region $r \in R^{V_i}_{T^b}$

\end{enumerate}

\end{definition}

Imagine that we have a graph whose vertex set is $\mathcal{A}$, then
the abstract next state function builds the edges among the abstract
states. Since the number of vertex is finite, model checking
algorithms are applicable.

\begin{definition}[Trace and run of abstract model]
A trace is an infinite sequence of abstract states: $\alpha_0
\rightarrow \alpha_1 \rightarrow \cdots $. The definitions of
prefix, suffix, equalities between traces and prefixes are similar
to those in definition \ref{Next_state_function_trace_run_def}.

\emph{\textbf{A run $\varsigma$ is a trace such that $\forall t\in
T: \varsigma[0]_c(t) = \varsigma[0]_p(t) = \bot \wedge \forall i \in
\mathbb{N}: \varsigma[i+1]\in f^{\alpha}(\varsigma[i])$. The set of
all runs is denoted by $\Lambda$.}}[TODO Hai]

Given a run $\varsigma$, functions $E_{\varsigma}^{\alpha} :
\mathbb{N} \rightarrow Bool$ and $RT_{\varsigma}^{\alpha} :
\mathbb{N} \rightarrow R$ are defined in the same way as those in
definition \ref{Next_state_function_trace_run_def}.

\end{definition}

\subsection{Definitions of Properties in Abstract Model}

Based on the abstract model, we have the following corresponding
property definitions.

\begin{definition}[Conflict free of abstract model]
The abstract model is conflict free iff $\forall C \in X, r_1\in C,
r_2 \in C, \varsigma \in \Lambda,i\in \mathbb{N}: r_1 \neq r_2
\rightarrow \neg (r_1 \in RT_\varsigma^{\alpha}(i) \wedge  r_2 \in
RT_\varsigma^{\alpha}(i))$.
\end{definition}

\begin{definition}[Dead rule of abstract model]
A rule $r$ is a dead rule of the abstract model iff $\forall
\varsigma \in \Lambda,i\in \mathbb{N}: r \not\in
RT_\varsigma^{\alpha}(i)$.
\end{definition}

\begin{definition}[Termination of abstract model]
The abstract model terminates iff $\forall \varsigma \in
\Lambda,i\in \mathbb{N}: (\forall j\in \mathbb{N}: i \le j
\rightarrow E_\varsigma^{\alpha}(j) = false) \rightarrow (\exists
k\in \mathbb{N}: i \le k \wedge RT_\varsigma^{\alpha}(k) = \emptyset
)$.
\end{definition}

\begin{definition}[Dead lock of abstract model]
The abstract model has dead lock iff ~$\exists \varsigma \in
\Lambda, i \in \mathbb{N}: (\forall \varsigma' \in
\Lambda:\varsigma[\cdots i] = \varsigma'[\cdots i] \rightarrow
\forall j\in \mathbb{N}:i \le j \rightarrow
RT_{\varsigma'}^{\alpha}(j)=\emptyset )$.
\end{definition}

Some relations between the two versions of definitions of properties
are given in the following theorems.

\begin{theorem}

A scenario is conflict free iff its abstract model is conflict free.
A scenario terminate iff its abstract model terminates. A scenario
has dead lock iff its abstract model has dead lock. A rule $r$ is a
dead rule of a scenario iff $r$ is a dead rule of its abstract
model.

\end{theorem}
\label{theorem1}
\begin{proof}
Omitted for now. [TODO Hai]
\end{proof}


\subsection{Verification Algorithms}

$G=(\mathcal {A}, E)$ is a graph with $\mathcal {A}$ (defined in
definition \ref{Ab_states}) is the set of vertex and $E \subseteq
\mathcal {A} \times 2^R \times \{true, false\} \times \mathcal {A}$
is the set of edges.







\end{document}
